// -*- C++ -*-
#include "circuit.h"
#include <cmath>

//_____________ Implementation of Simulink Blocks Semantics __________________
//

// The Abs block outputs the absolute value of the input.
//
// Not implemented:
// For signed data types, the absolute value of the most negative value
// is problematic since it is not representable by the data type. In this case,
// the behavior of the block is controlled by the Saturate
// on integer overflow check box. If checked, the absolute value of
// the data type saturates to the most positive representable value. If not checked,
// the absolute value of the most negative value represented by the data type
// has no effect.For example, suppose the block input is an 8-bit signed integer. The
// range of this data type is from -128 to 127, and the absolute value of -128
// is not representable. If you select the Saturate on
// integer overflow check box, then the absolute value of -128 is
// 127. If it is not selected, then the absolute value of -128 remains at -128.
// 
// Number of Inputs		1
// Number of Outputs		1
// Input Data Type(s)		Any except Boolean
// Output Data Type(s)		Any except Boolean
// MATLAB Function Called	None
// Sample Time Dependence	No
// Vectorized			Yes
template< typename T >
struct Abs : Value< T > {
    In< T > in;

    virtual T get( int i = 0 ) {
        return std::fabs(in->get( i ));
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( 1 );
    op.type = divine::OP;
    op.op = divine::ABS;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp = in->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    return id;
  }
};

// The Constant block generates a real or complex constant value.
//
// Not implemented:
// The block generates scalar (one-element array), vector (1-D array), or matrix
// (2-D array) output, depending on the dimensionality of the Constant
// value parameter and the setting of the Interpret
// vector parameters as 1-D parameter. Also, the block can
// generate either a sample-based or frame-based signal, depending on the setting
// of the Sampling mode parameter.The output of the block has the same dimensions 
// and elements as the Constant value parameter. If you specify a vector for
// this parameter, and you want the block to interpret it as a vector (i.e.,
// a 1-D array), select the Interpret vector parameters
// as 1-D parameter; otherwise, the block treats the Constant
// value parameter as a matrix (i.e., a 2-D array).
//
// C++ specifics:
// The default value is 1.
//
// 	Number of Inputs	0
// 	Number of Outputs	1
// 	Input Data Type(s)	None
// 	Output Data Type(s)	All
// 	Sample Time Dependence	No
// 	Vectorized		Yes
template< typename T >
struct Constant : virtual Value< T >, virtual In< T > {
    T value;
    virtual T get( int i = 0 ) {
      return value;
    }
    Constant() : value( 1 ) {}
    Constant( T v ) : value( v ) {}
    Constant< T > &operator=( T t ) { value = t; return *this; }

  virtual int build( divine::Expr *e ) {
    divine::Node con( 0 );
    con.value = value;
    con.type = divine::CON;
    e->nodes.push_back( con );
    return (e->nodes.size() - 1);
  }
};

// A type-cast block.
template< typename From, typename To >
struct DataTypeConversion : Value< To > {
    InSet< From, 1 > in;

    virtual To get( int i = 0 ) {
        return static_cast< To >( (*in.begin())->get( i ) );
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( 1 );
    op.type = divine::OP;
    op.op = divine::CAST;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    //std::cout << "??" << id << "?" << std::endl;
    int temp = (*in.begin())->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    return id;
  }
};

// The Gain Block provides a fixed gain value which is multiplied by the input to produce the output.
//
// 	Number of Inputs:	1
// 	Number of Outputs:	1
// 	Input Data Type(s):	Any except Boolean
// 	Output Data Type(s):	Any except Boolean 
// 	Sample Time Dependence:	Yes
// 	Vectorized:		Yes
template< typename T >
struct Gain : Value< T > {
    InSet< T, 1 > in;
    T value;

    virtual T get( int i = 0 ) {
        return value * (*in.begin())->get( i );
    }

    Gain( T v ) : value( v ) {}

  virtual int build( divine::Expr *e ) {
    divine::Node op( 2 );
    op.type = divine::OP;
    op.op = divine::TIMES;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    divine::Node con( 0 );
    con.type = divine::CON;
    con.value = value;
    e->nodes.push_back( con );
    int temp = e->nodes.size() - 1;
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    temp = (*in.begin())->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    return id;
  }
};

// The Ground Block is used to "ground" an input port, to prevent warning messages about unconnected inputs.
//
// The GROUND block is used to "ground" unused input ports. Doing so will prevent warnings about unconnected input ports. The GROUND block will output a zero value.
//
// 	Number of Inputs	0
// 	Number of Outputs	1
// 	Input Data Type(s)	None
// 	Output Data Type(s)	All
// 	Sample Time Dependence	No
// 	Vectorized		No
template< typename T >
struct Ground : virtual In< T > {
    virtual T get( int i = 0 ) {
      return 0;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node con( 0 );
    con.type = divine::CON;
    con.value = 0;
    e->nodes.push_back( con );
    return (e->nodes.size() - 1);
  }
};

// An input *block* (not a port).
template< typename T >
struct Inport : virtual Value< T >, virtual In< T >, virtual Stateful,
  virtual Referenceable {
  T value, first, last;
  std::string sname;

  virtual T get( int i = 0 ) {
    if ( tab )
      return symSet->getInport( i, name );
    else
      return value;
  }

    Inport() : value() {}
    Inport( T t ) : value( t ) {}
  
  Inport( T _first, T _last, std::string _n ): first( _first ), last( _last ),
                                               sname( _n ) {}

  void reg_sizes() {
    name = tab->ackn( first, last );
  }
  
    Inport< T > &operator=( T t ) { value = t; return *this; }
    void tick() {}
    void read( char *from ) {
        value = *(T *)from;
    }

    std::string print() {
          std::stringstream s;
          s <<  "\E[31m\033[1m" <<get() << "\033[0m";
          return s.str();
    }

  void top( divine::SMTRep *s, divine::Expr *e ) {
    uint32_t c = 0;
    int index = s->os.size() - 1;
    divine::Node andN( divine::OP, divine::AND, 2, c+1, c+2 );
    c+=2;
    e->nodes.push_back( andN );
    divine::Node geN( divine::OP, divine::GE, 2, c+1, c+2 );
    c+=2;
    e->nodes.push_back( geN );
    divine::Node ltN( divine::OP, divine::LE, 2, c+1, c+2 );
    e->nodes.push_back( ltN );
    divine::Node vN( divine::VAR, index );
    e->nodes.push_back( vN );
    divine::Node cN( divine::CON, first );
    e->nodes.push_back( cN );
    e->nodes.push_back( vN );
    divine::Node cN2( divine::CON, last );
    e->nodes.push_back( cN2 );

    divine::SMTRep::NFO n( *e, sname, divine::INP );
    s->os.push_back( n );
  }

  virtual int build( divine::Expr *e ) {
    divine::Node var( divine::VAR, name );
    e->nodes.push_back( var );
    return (e->nodes.size() - 1);
  }
};

template< typename T >
struct Logic: Value< T > {
    InSet< T, 18 > in;
    int sum;
    enum Function { AND, OR, XOR, NAND, NOR, NOT };
    Function f;

    Logic( Function _f ) : f( _f ) {}
 
    virtual T get( int j = 0 ) {
	switch (f) {
	  case AND:
	        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
        	    if (!(*i)->get( j )) return 0;
		return 1;
		break;
          case OR:
	        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
        	    if ((*i)->get( j )) return 1;
	        return 0;
		break;
	  case XOR:
	        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
        	    if ((*i)->get( j )) sum++;
		if (sum == 1) return 1;
		else return 0;
		break;
	  case NAND:
	        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
        	    if (!(*i)->get( j )) return 1;
		return 0;
		break;
          case NOR:
	        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
        	    if ((*i)->get( j )) return 0;
	        return 1;
		break;
	  case NOT:
	        return (! (*in.begin())->get( j ));
		break;
          default:
		return false; // TODO this should not be reached
		break;
	}
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( f == NOT ? 1 : in.size() );
    op.type = divine::OP;
    switch ( f ) {
    case AND:
      op.op = divine::AND;
      break;
    case OR:
      op.op = divine::OR;
      break;
    case XOR:
      op.op = divine::XOR;
      break;
    case NAND:
      op.op = divine::NAND;
      break;
    case NOR:
      op.op = divine::NOR;
      break;
    case NOT:
      op.op = divine::NOT;
      break;
    }
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < op.arity; i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

template< typename T >
struct LogicAnd: Value< T > {
    InSet< T, 18 > in;
 
    virtual T get( int i = 0 ) {
        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
       	    if (!(*i)->get( i )) return 0;
	return 1;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::AND;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

template< typename T >
struct LogicOr: Value< T > {
    InSet< T, 18 > in;
 
    virtual T get( int i = 0 ) {
        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
       	    if ((*i)->get( i )) return 1;
	return 0;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::OR;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ){
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

template< typename T >
struct LogicXor: Value< T > {
    InSet< T, 18 > in;
    int sum;

    virtual T get( int i = 0 ) {
        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
       	    if ((*i)->get( i )) sum++;
	if (sum == 1) return 1;
	else return 0;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::XOR;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

template< typename T >
struct LogicNand: Value< T > {
    InSet< T, 18 > in;

    virtual T get( int i = 0 ) {
        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
       	    if (!(*i)->get( i )) return 1;
	return 0;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::NAND;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

template< typename T >
struct LogicNor: Value< T > {
    InSet< T, 18 > in;
 
    virtual T get( int i = 0 ) {
        for ( typename InSet< T, 18 >::iterator i = in.begin(); i != in.end(); ++i )
       	    if ((*i)->get( i )) return 0;
        return 1;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::NOR;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

template< typename T >
struct LogicNot: Value< T > {
    InSet< T, 1 > in;
 
    virtual T get( int i = 0 ) {
	return (! (*in.begin())->get( i ));
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( 1 );
    op.type = divine::OP;
    op.op = divine::NOT;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp = (*in.begin())->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    return id;
  }
};

template< typename T >
struct Math : Value< T > {
    InSet< T, 2 > in;
    enum Function { pow, sqrt };
    Function f;

    Math( Function _f ) : f( _f ) {}
    T get( int i = 0 ) {
        switch (f) {
        case pow:
		return  std::pow ( (*in.begin())->get( i ), (*(in.begin()+1))->get( i ) );
                break;
        case sqrt:
		return  std::sqrt ( (*in.begin())->get( i ) );
                break;
         default:
		return false; // TODO this should not be reached
		break;
        }
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( f == pow ? 2 : 1 );
    op.type = divine::OP;
    op.op = (f == pow ? divine::POW : divine::SQRT);
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp = (*in.begin())->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    if ( op.op == divine::POW ) {
      temp = (*(in.begin() + 1))->build( e );
      e->nodes.at( id ).heirs.at( 1 ) = temp;
    }
    return id;
  }
};

// The Minimum/Maximum Value Block is used to determine the minimum/maximum value of two or more inputs.
//
// 	Number of Inputs:	2 (min), 99 (max)
// 	Number of Outputs:	1
// 	Input Data Type(s):	Any except Boolean
// 	Output Data Type(s):	Any except Boolean 
// 	MATLAB Function Called:	hwbcalib_minmax.m
// 	Sample Time Dependence:	No
// 	Vectorized:		Yes
template< typename T >
struct MinMax : Value< T > {
    InSet< T, 99 > in;
    enum Function { min, max };
    Function f;

    MinMax( Function _f ) : f( _f ) {}
    T get( int j = 0 ) {
	T out = (*in.begin())->get( j );
	switch (f) {
	case min:
	        for ( typename InSet< T, 99 >::iterator i = in.begin(); i != in.end(); ++i )
        	    out = std::min( out, (*i)->get( j ) );
		break;
	case max:
	        for ( typename InSet< T, 99 >::iterator i = in.begin(); i != in.end(); ++i )
        	    out = std::max( out, (*i)->get( j ) );
		break;
	default:
		return false; // TODO this should not be reached
	}
	return out;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = (f == min ? divine::MIN : divine::MAX);
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};


// The Multiport Switch Block provides a switching function among multiple input signals.
//
// The Multiport Switch block chooses between a number of inputs. The first
// input is called the control input, while the rest of
// the inputs are called data inputs. The value of the control
// input determines which data input is passed through to the output port. (See Changing the Orientation of a Block in
// Using Simulink for a description of the port order for various block orientations.) If the control input is an integer value, then the specified data input
// is passed through to the output. For example, suppose the Use
// zero-based indexing parameter is not selected. If the control input
// is 1, then the first data input is passed through to the
// output. If the control input is 2, then the second data
// input is passed through to the output, and so on. If the control input is
// not an integer value, the block first truncates the value to an integer by
// rounding to floor. If the truncated control input is less than 1 or
// greater than the number of input ports, an out-of-bounds error is returned.You specify the number of data inputs with the Number
// of input ports parameter. The data inputs can be scalar or vector.
// The block output is determined by these rules:If you specify only one data input and that input is a vector,
// the block behaves as an "index selector," and not as a multi-port switch.
// The block output is the vector element that corresponds to the value of the
// control input.If you specify more than one data input, the block behaves
// like a multi-port switch. The block output is the data input that corresponds
// to the value of the control input. If at least one of the data inputs is a
// vector, the block output is a vector. Any scalar inputs are expanded to vectors.If the inputs are scalar, the output is a scalar.The Index Vector block, also in the
// Signal Routing library, is another implementation of the Multiport Switch
// block that has different default parameter settings.
//
// Number of Inputs		3+
// Number of Outputs		1
// Input Data Type(s)		Any (all ports except the first one must be same), Boolean only (port 1)
// Output Data Type(s)		Any out (the same as input ports)
// MATLAB Function Called	hwbcalib_switch.m
// Sample Time Dependence	No
// Vectorized			Yes
template< typename T >
struct MultiPortSwitch : Value< T > {
    InSet< T, 99 > in;
    int number_of_inputs;
    // TODO implement also Simulink version: //  criterion  u2 >= treshold / u2 > treshold / u2 ~=0
    // TODO guarantee that the switch has only number of inputs on creation
    // double treshold;
    MultiPortSwitch( T t ) : number_of_inputs( t ) {}

    T get( int i = 0 ) { // TODO the control of the switch block is fixed to be second input which is valid for HAM switch block
	return (*(in.begin()+(*(in.begin()))->get( i )))->get( i );
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( number_of_inputs );
    op.type = divine::OP;
    op.op = divine::MSWITCH;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

// A simple output *block*.
template< typename T >
struct Outport : Value< T >, virtual Referenceable {
  std::string name;
    InSet< T, 1 > in;
    virtual T get( int i = 0) {
      return (*in.begin())->get( i );
    }

  void top( divine::SMTRep *s, divine::Expr *e ) {
    build( e );
    divine::SMTRep::NFO n( *e, name, divine::OUT );
    s->os.push_back( n );
  }

  virtual int build( divine::Expr *e ) {
    (*in.begin())->build( e );
  }

  Outport() {}
  Outport( std::string n ): name( n ) {}
};


// The Product Block is used to multiply two or more input signals.
// This block is used to multiply inputs. Note that the number of ports input to this block must be between 2 and 20.
//
// 	Number of Inputs:	2 (min), 20 (max)
// 	Number of Outputs:	1
// 	Input Data Type(s):	Any except Boolean (All must be same type)
// 	Output Data Type(s):	Any except Boolean 
// 	MATLAB Function Called:	hwbcalib_product.m
// 	Sample Time Dependence:	No
// 	Vectorized:		Yes
template< typename T >
struct Product : Value< T > {
    InSet< T, 20 > in;

    virtual T get( int j = 0 ) {
	T out = 1;	// 1 is an identity element for multiplication
        for ( typename InSet< T, 20 >::iterator i = in.begin(); i != in.end(); ++i )
            out = out * (*i)->get( j );
        return out;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::TIMES;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};
 
// The Relational Operator Block is used to compare the values of two inputs.
//
// For "lessThan" function:
// If input A is less than input B, then a one is output, otherwise a zero is output.
// For "greaterThan" function:
// If input A is greater than input B, then a one is output, otherwise a zero is output.
//
// Number of Inputs	 	2
// Number of Outputs	 	1
// Input Data Type(s)	 	Any (Both the input must be same)
// Output Data Type(s)	 	Boolean
// MATLAB Function Called	None
// Sample Time Dependence	No
// Vectorized		 	Yes
template< typename T >
struct RelationalOperator : Value< bool > {
    InSet< T, 2 > in;
    enum Function { LT, LE, GT, GE };
    Function f;

    RelationalOperator( Function _f ) : f( _f ) {}

    bool get( int i = 0 ) {
        switch (f) {
        case LT:
		return ((*in.begin())->get( i ) <  (*(in.begin()+1))->get( i )?true:false); break;
        case LE:
		return ((*in.begin())->get( i ) <= (*(in.begin()+1))->get( i )?true:false); break;
        case GT:
		return ((*in.begin())->get( i ) >  (*(in.begin()+1))->get( i )?true:false); break;
        case GE:
		return ((*in.begin())->get( i ) >= (*(in.begin()+1))->get( i )?true:false); break;
	default:
		return false; // TODO this should not be reached
	}
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( 2 );
    op.type = divine::OP;
    switch ( f ) {
    case LT:
      op.op = divine::LT;
      break;
    case LE:
      op.op = divine::LE;
      break;
    case GT:
      op.op = divine::GT;
      break;
    case GE:
      op.op = divine::GE;
      break;
    }
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};


template< typename T >
struct Rounding : Value< T > {
    InSet< T, 1 > in;
    enum Function { ceil, floor, round, fix };
    Function f;

    Rounding( Function _f ) : f( _f ) {}
    T get( int i = 0 ) {
        switch (f) {
        case ceil:
		return std::ceil((*in.begin())->get( i ));
                break;
        case floor:
		return std::floor((*in.begin())->get( i ));
                break;
        case round:
		return std::floor((*in.begin())->get( i ) + 0.5);
                break;
        case fix:
		return (*in.begin())->get( i )>0?std::floor((*in.begin())->get( i )):std::ceil((*in.begin())->get( i ));;
                break;
	default:
		return false; // TODO this should not be reached
        }
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( 1 );
    op.type = divine::OP;
    switch ( f ) {
    case ceil:
      op.op = divine::CEIL;
      break;
    case floor:
      op.op = divine::FLOOR;
      break;
    case round:
      op.op = divine::ROUND;
      break;
    case fix:
      op.op = divine::FIX;
      break;
    }
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp = (*in.begin())->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    return id;
  }
};

// Saturation Block limits range of signal
//
// 	Number of Inputs:	1
// 	Number of Outputs:	1
// 	Input Data Type(s):	Any except Boolean
// 	Output Data Type(s):	Any except Boolean 
// 	Sample Time Dependence:	Yes
// 	Vectorized:		Yes
template< typename T >
struct Saturate : Value< T > {
    InSet< T, 1 > in;
    T lower_limit, upper_limit;

    virtual T get( int i = 0 ) {
        return std::max( std::min( (*in.begin())->get( i ), upper_limit), lower_limit );
    }

    Saturate( T l, T u ) : lower_limit( l ), upper_limit( u ) {}

  virtual int build( divine::Expr *e ) {
    divine::Node op( 3 );
    op.type = divine::OP;
    op.op = divine::BEET;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp = (*in.begin())->build( e );
    e->nodes.at( id ).heirs.at( 0 ) = temp;
    divine::Node con( 0 );
    con.type = divine::CON;
    con.value = lower_limit;
    e->nodes.push_back( op );
    e->nodes.at( id ).heirs.at( 1 ) = e->nodes.size() - 1;
    con.value = upper_limit;
    e->nodes.push_back( op );
    e->nodes.at( id ).heirs.at( 2 ) = e->nodes.size() - 1;
    return id;
  }
};

// Sum
// Add or subtract inputs
//
// The Sum block performs addition or subtraction on its inputs. This block can add or subtract scalar, vector, or matrix inputs. It can also collapse the elements of a single input vector.
//
// You specify the operations of the block with the List of Signs parameter. Plus (+), minus (-), and spacer (|) characters indicate the operations to be performed on the inputs:
//
// If there are two or more inputs, then the number of characters must equal the number of inputs. For example, "+-+" requires three inputs and configures the block to subtract the second (middle) input from the first (top) input, and then add the third (bottom) input. 
//
// All nonscalar inputs must have the same dimensions. Scalar inputs will be expanded to have the same dimensions as the other inputs.
//
// A spacer character creates extra space between ports on the block's icon.
//
// If only addition of all inputs is required, then a numeric parameter value equal to the number of inputs can be supplied instead of "+" characters.
//
// If only one vector is input, then a single "+" or "-" will collapse the vector using the specified operation.
//
// The Sum block first converts the input data type(s) to the output data type using the specified rounding and overflow modes, and then performs the specified operations.
//
// 	
// 	Number of Inputs:	1 (min), 25 (max)
// 	Number of Outputs:	1
// 	Input Data Type(s):	Any except Boolean (must all be the same) 
// 	Output Data Type(s):	Any except Boolean 
// 	MATLAB Function Called:	hwbcalib_sum.m
// 	Sample Time Dependence:	No
// 	Vectorized:		Yes
template< typename T >
struct Sum : Value< T > {
    InSet< T, 25 > in;

    virtual T get( int j = 0 ) {
        T out = 0;	// 0 is an identity element for addition
        for ( typename InSet< T, 25 >::iterator i = in.begin(); i != in.end(); ++i )
            out += (*i)->get( j );
        return out;
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( in.size() );
    op.type = divine::OP;
    op.op = divine::PLUS;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    //std::cout << "id:" << id << std::endl;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      //std::cout << "temp: " << temp << std::endl;
      e->nodes.at( id ).heirs.at( i ) = temp;//in.at( i )->build( e );
    }
    // std::cout << "id:" << id << " " << e->nodes.at( id ).heirs.at( 0 ) << " "
    //           << e->nodes.at( id ).heirs.at( 1 ) << std::endl;
    return id;
  }
};

// The Switch Block provides a switching function between two input signals.
//
// The SWITCH block passes the Normally Closed (NC) input to the output when the switch control input is 0.  The Normally Open (NO) input is passed to the output when the switch control input is 1.  A threshold value of 0.5 is used to determine whether the control input is 1 or 0.  The order of the inputs is selectable to allow either the NO or NC input to be first. The block's icon indicates which input is the "normally closed" input, by means of the line connecting one of the top two input ports to the output port.
//
// Number of Inputs		3
// Number of Outputs		1
// Input Data Type(s)		Any (ports 1&2 must be same), Boolean only (port 3)
// Output Data Type(s)		Any out
// MATLAB Function Called	hwbcalib_switch.m
// Sample Time Dependence	No
// Vectorized			Yes
template< typename T >
struct Switch : Value< T > {
    InSet< T, 3 > in;
    // TODO implement Simulink version: //  criterion  u2 >= treshold / u2 > treshold / u2 ~=0
    // double treshold;

    T get( int i = 0 ) { // TODO the control of the switch block is fixed to be second input which seems to be correct for HAM switch block
	return ((*(in.begin()+1))->get( i ))?(*in.begin())->get( i ):(*(in.begin()+2))->get( i );
    }

  virtual int build( divine::Expr *e ) {
    divine::Node op( 3 );
    op.type = divine::OP;
    op.op = divine::SWITCH;
    e->nodes.push_back( op );
    int id = e->nodes.size() - 1;
    int temp;
    for ( int i = 0; i < in.size(); i++ ) {
      temp = in.at( i )->build( e );
      e->nodes.at( id ).heirs.at( i ) = temp;
    }
    return id;
  }
};

// The Unit Delay Block provides a function which holds data for use in the next computational frame.
//
// The Unit Delay Block is used to provide a unit delay function without the ability to provide a reset.  The block's initial condition output is set. The block will accept any input signal datatype, and will output the same type.
//
// 	Number of Inputs		1
// 	Number of Outputs		1
// 	Input Data Type(s)		Any 
// 	Output Data Type(s)		Any 
// 	MATLAB Function Called	None
// 	Sample Time Dependence	Yes
// 	Vectorized			Yes
template< typename T >
struct UnitDelay : virtual Value< T >, virtual Clock, virtual Stateful,
  virtual Referenceable {
    InSet< T, 1 > in;
    T last;
  std::string sname;
  virtual T get( int i = 0 ) {
    if ( tab )
      return symSet->getDelay( i, name );
    else
      return last;
  }

  void top( divine::SMTRep *s, divine::Expr *e ) {
    (*in.begin())->build( e );
    divine::SMTRep::NFO n( *e, sname, divine::DEL );
    s->os.push_back( n );
  }

  virtual int build( divine::Expr *e ) {
    divine::Node var( 0 );
    var.type = divine::VAR;
    var.name = name;
    e->nodes.push_back( var );
    return (e->nodes.size() - 1);
  }

    void tick() {
      if ( tab ) {
        for ( int i = 0; i < symSet->inputs.size(); i++ ) {
          T gget = (*in.begin())->get( i );
          symSet->partial.at( i ).at( name ) = gget;
        }
      }
      else
        last = (*in.begin())->get();
    }
  
    void read( char *from ) {
        last = *(T *)from;
    }

  UnitDelay() : last() {}
  UnitDelay( std::string n ) : last(), sname( n ) {}

  void reg_sizes() {
    name = tab->ackn( sizeof( T ) );
  }
};


// The Variable Asymmetrical Limiter Block provides a magnitude limiter with limits which are independently input to the block as input signals.
//
// The VARIABLE ASYMMETRICAL LIMITER block provides upper and lower bounds for a signal. The upper and lower bounds are defined by the two LIM inputs, with the greater of the two LIM inputs being the upper bound and the lesser of the two LIM inputs being the lower bound. If the input is between the bounds it is passed to the output.  If the input is greater than the upper bound, the output is set equal to the upper bound. If the input is less then the lower bound the output is set equal to the lower bound. The order of the input limits (i.e. which is greater, which is less) does not matter. Input signals outside of the limit boundaries will be output as the nearest boundary value.
//
// Number of Inputs		3
// Number of Outputs		1
// Input Data Type(s)		Double only
// Output Data Type(s)		Double only
// MATLAB Function Called	None
// Sample Time Dependence	No
// Vectorized			Yes
//
//
//
// The Asymmetrical Limiter Block provides a magnitude limiter with upper and lower limits (bounds) which are user-specified using the block's GUI and Input between the upper and lower bounds is passed-through.
//
// The ASYMMETRICAL LIMITER Block provides upper and lower bounds for a signal. If the input is between the boundaries, it is passed directly to the output. If the input is greater than the upper bound, it will be output as the upper boundary value.  If the input is less than the lower bound, it will be output as the lower boundary value. This block will accept any inputs except Boolean, and is vectorized.
//
// Number of Inputs		1
// Number of Outputs		1
// Input Data Type(s)		Any except Boolean
// Output Data Type(s)		Any except Boolean
// MATLAB Function Called	hwbcalib_asymmetriclimit.m
// Sample Time Dependence	No
// Vectorized			Yes
// NOTHING

/********************************************************************
 * Stateflow models require a Terminator block
 * It was left the same as Outport in order to avoid typing problems
 ********************************************************************/
template< typename T >
struct Terminator : Value< T > {
    InSet< T, 1 > in;
    virtual T get( int i = 0 ) {
      return (*in.begin())->get( i );
    }

  virtual int build( divine::Expr *e ) {
    int temp = (*in.begin())->build( e );
    return temp;
  }
};

/********************************************************************
 * Stateflow models require a Demux block
 * It was left the same as Outport in order to avoid typing problems
 ********************************************************************/
template< typename T >
struct Demux : Value< T > {
    InSet< T, 1 > in;
    virtual T get( int i = 0 ) {
      return (*in.begin())->get( i );
    }

  virtual int build( divine::Expr *e ) {
    int temp = (*in.begin())->build( e );
    return temp;
  }
};


